\begin{tabbing}
$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$(?$E$)), $a$,$b$,$e$:$E$.
\\[0ex]SWellFounded(($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$) $\in$ $E$))
\\[0ex]$\Rightarrow$ \=(l\_before($a$; $b$; eventlist(${\it pred?}$; $e$); $E$)\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(($a$ rel\_star($E$; ($\lambda$$x$,$y$. ($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$) $\in$ $E$))) $e$)\+
\\[0ex]$\wedge$ ($b$ rel\_star($E$; ($\lambda$$x$,$y$. ($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$) $\in$ $E$))) $e$)
\\[0ex]$\wedge$ ($a$ rel\_plus($E$; ($\lambda$$x$,$y$. ($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$) $\in$ $E$))) $b$)))
\-\-
\end{tabbing}